Strand space theory relies on individual judgments and subjective experiences much, and can hardly be automated. To solve this problem, a more formal and objective verification process based on strand space theory and authentication test was proposed. First, a set of type labels was defined for terms of protocol to expand strand space and authentication test theory. By listing all possible occurrences of test instances, checking agreement of arguments in test component, verifying uniqueness of transforming edge, examining agreement of arguments in goal strand, protocols verification process based on strand space could be formalized to a series of programmable procedures. Time complexity of the whole verification algorithm is O(n²), hence state space explosion problem common in state space search was avoided. On the basis of theoretical study, an automatic tool was implemented to verify authentication attributes of security protocols automatically. BAN-Yahalom protocol and TLS handshake protocol 1.0 were analyzed as examples, where a new attack to BAN-Yahalom was found. It is similar to Syverson's attack, but it has no restriction on server's verification of nonce, hence has more general application scenario than Syverson's.